T:Type, E:(TT).
(x, y:T. Dec(E(x,y)))  (f:TT. (x, y:T. ((x f y))  E(x,y))) 

latex

Up	quot 1, quot 1
Definitions	t  T, P  Q, P  Q, P & Q, x f y, x:A. B(x), x(s1,s2), P  Q, , x:A. B(x), P  Q, if b then t else f fi , tt, b, True, ff, Dec(P), False, A
Lemmas	assert wf, iff wf, bool wf, decidable wf, bfalse wf, btrue wf, not wf, true wf, false wf, decidable functionality, decidable assert